Nuprl Lemma : concat_wf 11,40

T:Type, ll:(T List List). concat(ll (T List) 
latex


Definitionsx:AB(x), t  T, concat(ll)
Lemmasreduce wf, append wf

origin